w:World, p:FairFifo, e:E, l:IdLnk. w_sends(e;l)  {m:Msg| mlnk(m) = l } List 

latex

Definitions	Msg, IdLnk, s = t, xL. P(x), mlnk(m), t  T, x:A. B(x), Prop, x.A(x), w_sends(e;l), P  Q, x. t(x), World, FairFifo, E, {x:A| B(x) }, type List, <a,b>, x:AB(x), S  T, x:AB(x), Msg(M), Type, True, T, (x  l), P  Q, P & Q, P  Q, loc(e), w.M, source(l), Id, time(e), m(i;t), a = b, b, onlnk(l;mss)
Lemmas	assert-eq-lnk, member filter, eq lnk wf, w-m wf, w-time wf, Msg wf, Id wf, lsrc wf, mlnk wf, w-M wf, w-loc wf, l member wf, squash wf, true wf, w-sends-lemma, w-E wf, fair-fifo wf, world wf, list-set-type2, w sends wf, IdLnk wf, w-Msg wf